Definitions | x:A. B(x), t T, l_before(x; y; l; T), (x l), Type, no_repeats(T; l), P Q, x:AB(x), prop{i:l}, x:A B(x), P Q, P Q, P Q, type List, s = t, cons(car; cdr), [], tl(l), n - m, if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n + m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A, A B, , {x:A| B(x)} , , False, guard(T), P Q, left + right, x. t(x), True, T |